\begin{figure}[H]
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Require} \coqdockw{Export} \coqexternalref{}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.ZArith}{\coqdoclibrary{ZArith}}.\coqdoceol
\coqdocnoindent
\coqdockw{Require} \coqdockw{Import} \coqdoclibrary{Matrix}.\coqdoceol
\coqdocnoindent
\coqdockw{Require} \coqdockw{Import} \coqdoclibrary{Lenguaje}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Module} \coqdef{Tipos.Tipos}{Tipos}{\coqdocmodule{Tipos}} \<: \coqdocmodule{ITipos}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.Bool}{Bool}{\coqdocdefinition{Bool}} := \coqexternalref{bool}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.Integer}{Integer}{\coqdocdefinition{Integer}} := \coqexternalref{Z}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Numbers.BinNums}{\coqdocinductive{Z}}. \coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.Byte}{Byte}{\coqdocdefinition{Byte}} := \coqexternalref{Z}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Numbers.BinNums}{\coqdocinductive{Z}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.Matrix}{Matrix}{\coqdocdefinition{Matrix}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n} := \coqdocdefinition{Matrix.Matrix} \coqdocvariable{A} (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{m}) (\coqexternalref{Z.to nat}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.to\_nat}} \coqdocvariable{n}).\coqdoceol
\end{coqdoccode}
\textit{(* Más definiciones *)}\\
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.bool or}{bool\_or}{\coqdocdefinition{bool\_or}} := \coqexternalref{orb}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocdefinition{orb}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int minus}{int\_minus}{\coqdocdefinition{int\_minus}} := \coqexternalref{Z.sub}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.sub}}.\coqdoceol
\coqdocnoindent
\coqdockw{Definition} \coqdef{Tipos.Tipos.int mult}{int\_mult}{\coqdocdefinition{int\_mult}} := \coqexternalref{Z.mul}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.ZArith.BinInt}{\coqdocdefinition{Z.mul}}.\coqdoceol
\end{coqdoccode}
\textit{(* Más definiciones *)}\\
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{End} \coqref{Tipos}{\coqdocmodule{Tipos}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Module} \coqdef{Tipos.LenguajeImpl}{LenguajeImpl}{\coqdocmodule{LenguajeImpl}} := \coqdocmodule{Lenguaje.Lenguaje} \coqref{Tipos}{\coqdocmodule{Tipos}}.\coqdoceol
\coqdocnoindent
\coqdockw{Export} \coqdocvar{Tipos}.\coqdoceol
\coqdocnoindent
\coqdockw{Export} \coqdocvar{LenguajeImpl}.
\end{coqdoccode}
\caption{Módulo de implementación de tipos} \label{module:types}
\end{figure}